\begin{tabbing}
$\forall$${\it es}$:ES, ${\it Cmd}$:Type, ${\it In}$:AbsInterface(${\it Cmd}$), ${\it isupdate}$:(${\it Cmd}$$\rightarrow\mathbb{B}$), ${\it Sys}$, ${\it Out}$:AbsInterface(Top).
\\[0ex](E(${\it In}$) $\subseteq$r E(${\it Sys}$))
\\[0ex]$\Rightarrow$ \=($\forall$$f$:sys{-}antecedent(${\it es}$;${\it Sys}$).\+
\\[0ex]($\forall$$u$:E(${\it Sys}$). ($f$($u$) = $u$ $\in$ E) $\Leftarrow\!\Rightarrow$ ($\uparrow$($u$ $\in_{b}$ ${\it In}$)))
\\[0ex]$\Rightarrow$ \=($\forall$${\it chain}$:(E(${\it Sys}$)$\rightarrow$(Id List)).\+
\\[0ex]chain{-}consistent($f$;${\it chain}$)
\\[0ex]$\Rightarrow$ \=($\forall$$e$, ${\it e'}$:E(${\it Sys}$).\+
\\[0ex]($\neg$(loc($f$($e$)) = loc($e$) $\in$ Id))
\\[0ex]$\Rightarrow$ (loc(${\it e'}$) = loc($e$) $\in$ Id)
\\[0ex]$\Rightarrow$ \=($\forall$$b$:E(${\it Sys}$).\+
\\[0ex]($f$(${\it e'}$) $<$loc $f$($b$))
\\[0ex]$\Rightarrow$ ($f$($b$) $<$loc $f$($e$))
\\[0ex]$\Rightarrow$ ($\neg$(loc($f$($b$)) = loc($b$) $\in$ Id))
\\[0ex]$\Rightarrow$ (loc($b$) = loc($e$) $\in$ Id)))))
\-\-\-\-
\end{tabbing}